the_w:World, i:Id, a:Action(i), l:IdLnk. isrcv(l;a)  msg(a)  Msg 

latex

Definitions	Knd, kindcase(k; a.f(a); l,t.g(l;t) ), islocal(k), act(k), 1of(t), 2of(t), x. t(x), True, tag(k), valtype(i;a), w.M, isnull(a), isrcv(k), kind(a), p  q, Unit, P  Q, P & Q, , Prop, b, A, a = b, lnk(k), False, msg(a), P  Q, msg(l;t;v), val(a), Msg, b, isrcv(l;a), IdLnk, Action(i), x:A. B(x), Id, t  T, World
Lemmas	world wf, Id wf, w-action wf, IdLnk wf, w-isrcvl wf, assert wf, false wf, w-kind wf, lnk wf, eq lnk wf, isrcv wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, w-isnull wf, w-val wf, tagof wf, w-M wf, msg wf, true wf, pi2 wf, pi1 wf, subtype rel self, Knd wf